Nuprl Lemma : es-E-interface-predicate
11,40
postcript
pdf
es
,
B
,
I
:Top. {
e
:E| {
I
}(
e
)} ~ E(
I
)
latex
Definitions
x
:
A
.
B
(
x
)
,
{
I
}
,
E(
X
)
,
t
T
Lemmas
top
wf
origin
es, B, I:Top. {e:E| {I}(e)} ~ E(I) es, B, I:Top. {e:E| {I}(e)} ~ E(I) x:A. B(x)
T